/*
 *  SableJBDD, a Java Binary Decision Diagram package.
 *  Copyright (C) 2003  Feng Qian
 *
 *  This library is free software; you can redistribute it and/or
 *  modify it under the terms of the GNU Lesser General Public
 *  License as published by the Free Software Foundation; either
 *  version 2.1 of the License, or (at your option) any later version.
 *
 *  This library is distributed in the hope that it will be useful,
 *  but WITHOUT ANY WARRANTY; without even the implied warranty of
 *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 *  Lesser General Public License for more details.
 *
 *  You should have received a copy of the GNU Lesser General Public
 *  License along with this library; if not, write to the Free Software
 *  Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */
//$Id: JBDD.java,v 1.14 2004/03/15 02:06:54 fqian Exp $
package SableJBDD.bdd;

import java.util.*;
import java.io.*;

/**
 * A BDD object represents a bdd function. It has a root node and a manager, and
 * supports basic bdd operations.
 * 
 * @author Feng Qian
 */

public class JBDD {

	// a bdd operation can be implemented by apply function or ite function
	// if this option is on, some operations are implmenented using the ITE
	// function
	private static boolean USING_ITE_IMPLEMENTATION = false;

	/**
	 * Defines a BDD function with a specific BDD manager and a root node. A BDD
	 * function is created either by a BDD manager or the result of BDD
	 * operations.
	 * 
	 * @param manager
	 *            , the bdd manager of this function.
	 * @param node
	 *            , the root node of this function
	 */
	protected JBDD(JBddManager manager, JBddNode node) {
		this.bddm = manager;
		this.root = node;
	}

	// //////////////////////////////////////////////
	// Basic BDD operations
	// //////////////////////////////////////////////

	/**
	 * Returns a copy of current BDD with the same manager and same root node.
	 */
	public JBDD copy() {
		return new JBDD(this.bddm, this.root);
	}

	/**
	 * AND operation.
	 * 
	 * @param other
	 *            the second bdd function.
	 * @return this & other
	 */
	public JBDD and(JBDD other) {
		assert (this.bddm == other.bddm);

		if (USING_ITE_IMPLEMENTATION) {
			return new JBDD(this.bddm, this.bddm.ITE(this.root, other.root,
					JBddConstNode.ZERO()));
		} else {
			return new JBDD(this.bddm, this.bddm.AND(this.root, other.root));
		}
	}

	/**
	 * In-node AND operation in place.
	 * 
	 * @param other
	 *            the second bdd function
	 */
	public void andWith(JBDD other) {
		assert (this.bddm == other.bddm);

		if (USING_ITE_IMPLEMENTATION) {
			this.root = this.bddm.ITE(this.root, other.root, JBddConstNode
					.ZERO());
		} else {
			this.root = this.bddm.AND(this.root, other.root);
		}
	}

	/**
	 * OR operation.
	 * 
	 * @param other
	 *            the second bdd function.
	 * @return this | other
	 */
	public JBDD or(JBDD other) {
		assert (this.bddm == other.bddm);

		if (USING_ITE_IMPLEMENTATION)
			return new JBDD(this.bddm, this.bddm.ITE(this.root, JBddConstNode
					.ONE(), other.root));
		else
			return new JBDD(this.bddm, this.bddm.OR(this.root, other.root));
	}

	/**
	 * In-node OR operation.
	 * 
	 * @param other
	 *            the second bdd function
	 */
	public void orWith(JBDD other) {
		assert (this.bddm == other.bddm);
		if (USING_ITE_IMPLEMENTATION)
			this.root = this.bddm.ITE(this.root, JBddConstNode.ONE(),
					other.root);
		else
			this.root = this.bddm.OR(this.root, other.root);
	}

	/**
	 * NOT operation.
	 * 
	 * @return ! this
	 */
	public JBDD not() {

		if (USING_ITE_IMPLEMENTATION)
			return new JBDD(this.bddm, this.bddm.ITE(this.root, JBddConstNode
					.ONE(), JBddConstNode.ZERO()));
		else
			return new JBDD(this.bddm, this.bddm.NOT(this.root));
	}

	/**
	 * XOR operation.
	 * 
	 * @param other
	 *            the second bdd function.
	 * @return this (+) other
	 */
	public JBDD xor(JBDD other) {
		assert (this.bddm == other.bddm);
		return new JBDD(this.bddm, this.bddm.XOR(this.root, other.root));
	}

	/**
	 * In-node XOR operation.
	 * 
	 * @param other
	 *            the second bdd function.
	 */
	public void xorWith(JBDD other) {
		assert (this.bddm == other.bddm);
		this.root = this.bddm.XOR(this.root, other.root);
	}

	/**
	 * NAND operations, it is more efficient than AND followed by NOT.
	 * 
	 * @param other
	 *            the second bdd function.
	 * @return ! (this & other)
	 */
	public JBDD nand(JBDD other) {
		assert (this.bddm == other.bddm);
		return new JBDD(this.bddm, this.bddm.NAND(this.root, other.root));
	}

	/**
	 * In-node NAND operation.
	 * 
	 * @param other
	 *            the second bdd function.
	 */
	public void nandWith(JBDD other) {
		assert (this.bddm == other.bddm);
		this.root = this.bddm.NAND(this.root, other.root);
	}

	/**
	 * NOR operation, it is more efficient than OR followed by NOT.
	 * 
	 * @param other
	 *            the second bdd function.
	 * @return ! (this | other)
	 */
	public JBDD nor(JBDD other) {
		assert (this.bddm == other.bddm);
		return new JBDD(this.bddm, this.bddm.NOR(this.root, other.root));
	}

	/**
	 * In-node NOR operation.
	 * 
	 * @param other
	 *            the second bdd function.
	 */
	public void norWith(JBDD other) {
		assert (this.bddm == other.bddm);
		this.root = this.bddm.NOR(this.root, other.root);
	}

	/**
	 * IMPLY operation.
	 * 
	 * @param other
	 *            the second bdd function.
	 * @return this -> other
	 */
	public JBDD imply(JBDD other) {
		assert (this.bddm == other.bddm);

		if (USING_ITE_IMPLEMENTATION)
			return new JBDD(this.bddm, this.bddm.ITE(this.root, other.root,
					JBddConstNode.ONE()));
		else
			return new JBDD(this.bddm, this.bddm.IMPLY(this.root, other.root));
	}

	/**
	 * BIIMPLY operation.
	 * 
	 * @param other
	 *            the second bdd function.
	 * @return this <-> other
	 */
	public JBDD biimply(JBDD other) {
		assert (this.bddm == other.bddm);
		return new JBDD(this.bddm, this.bddm.BI_IMPLY(this.root, other.root));
	}

	/**
	 * DIFF operation.
	 * 
	 * @param other
	 *            the second bdd function.
	 * @return this / other
	 */
	public JBDD diff(JBDD other) {
		assert (this.bddm == other.bddm);
		return new JBDD(this.bddm, this.bddm.DIFF(this.root, other.root));
	}

	/**
	 * LESS operation.
	 * 
	 * @param other
	 *            the second bdd function.
	 * @return this < other
	 */
	public JBDD less(JBDD other) {
		assert (this.bddm == other.bddm);
		return new JBDD(this.bddm, this.bddm.LESS(this.root, other.root));
	}

	/**
	 * Inverse imply operation.
	 * 
	 * @param other
	 *            the second bdd function.
	 * @return this <- other
	 */
	public JBDD invimp(JBDD other) {
		assert (this.bddm == other.bddm);
		return new JBDD(this.bddm, this.bddm.IMPLY(other.root, this.root));
	}

	// //////////////////////////
	// Replace function
	// //////////////////////////
	/**
	 * Replaces a set of variables in this bdd to another set of variables.
	 * 
	 * @param varmap
	 *            a map from a set of variables to another set of variables,
	 *            where the variables of the first set in this bdd will be
	 *            replaced by the variables of the second set.
	 * @return the new bdd after replacement
	 * 
	 *         This method may fail if this bdd contains nodes of variables of
	 *         replacing targets.
	 */
	public JBDD replace(Map varmap) {
		return new JBDD(this.bddm, this.bddm.REPLACE(this.root, varmap));
	}

	// //////////////////////////
	// Quantifications
	// //////////////////////////
	/**
	 * Apply existential quantification on this bdd function.
	 * 
	 * @param vars
	 *            a bdd which is the conjunction of several variables' positive
	 *            form.
	 * @return the resulted bdd function
	 */
	public JBDD exist(JBDD vars) {
		return new JBDD(this.bddm, this.bddm.EXISTENTIAL(this.root, vars.root));
	}

	/**
	 * Apply universal quantification on this bdd function.
	 * 
	 * @param vars
	 *            a bdd which is the conjunction of several variables' positive
	 *            form.
	 * @return the resulted bdd function
	 */
	public JBDD forall(JBDD vars) {
		return new JBDD(this.bddm, this.bddm.UNIVERSAL(this.root, vars.root));
	}

	/**
	 * Apply unique quantification on this bdd function.
	 * 
	 * @param vars
	 *            a bdd which is the conjunction of several variables' positive
	 *            form.
	 * @return the resulted bdd function.
	 */
	public JBDD unique(JBDD vars) {
		return new JBDD(this.bddm, this.bddm.UNIQUE(this.root, vars.root));
	}

	// ///////////////////////////////////
	// query
	// //////////////////////////////////
	/**
	 * Checks if this BDD is ZERO
	 * 
	 * @return true if this is zero
	 */
	public boolean isZero() {
		return this.root == JBddConstNode.ZERO();
	}

	/**
	 * Checks if this BDD is ONE
	 * 
	 * @return true if this is one
	 */
	public boolean isOne() {
		return this.root == JBddConstNode.ONE();
	}

	/**
	 * Checks if the root is a particular variable
	 * 
	 * @return true if it is
	 */
	public boolean isRootOf(JBddVariable var) {
		return this.root.variable == var;
	}

	/**
	 * Counts the size of this bdd function (the number of internal nodes),
	 * excluding two sink nodes.
	 * 
	 * @return the size of this bdd function.
	 */
	public int size() {
		Set countedNodes = new HashSet();
		traverseBddNodes(this.root, countedNodes);
		return countedNodes.size();
	}

	// recursively traverses a bdd, collects unvisited nodes
	private void traverseBddNodes(JBddNode node, Set visited) {
		if (visited.contains(node))
			return;
		if (!node.isConst()) {
			visited.add(node); // exclude constants
			traverseBddNodes(node.low, visited);
			traverseBddNodes(node.high, visited);
		}
	}

	/**
	 * Dumps this bdd to a DOT format graph.
	 * 
	 * @param out
	 *            the output stream
	 * @param graphname
	 *            the name in DOT graph
	 */
	public void toDotGraph(PrintStream out, String graphname) {
		out.println("digraph " + graphname + " {");
		out.println("graph[label=\"" + graphname + "\"];");

		Set visitedNodes = new HashSet();
		printEdgesInternal(out, this.root, visitedNodes);

		out.println("}");
	}

	public void toDotGraphOverriden(PrintWriter out, String graphname) {
		Set visitedNodes = new HashSet();
		// printEdgesInternalOverriden(out, this.root, visitedNodes);
		printBreadthFirstTraversal(out, this.root, visitedNodes);
	}

	// recursively traverse the diagram and print out edges if it was
	// not printed before.
	private void printEdgesInternal(PrintStream out, JBddNode node,
			Set<JBddNode> visited) {

		if (visited.contains(node))
			return;
		visited.add(node);

		if (!node.isConst())
			out.print(node.getUniqueId() + "[label=\"" + node.getLevel()
					+ "\"];");
		else
			out.print(node.getUniqueId() + "[label=\"" + node + "\"];");

		if (!node.isConst()) {
			out.println(node.getUniqueId() + "[shape=circle];");
			out.print(node.getUniqueId() + " -> " + node.low.getUniqueId());
			out.println("[style=dotted];");
			out.print(node.getUniqueId() + " -> " + node.high.getUniqueId());
			out.println("[style=solid];");

			printEdgesInternal(out, node.low, visited);
			printEdgesInternal(out, node.high, visited);
		} else {
			out.println(node.getUniqueId() + "[shape=box,style=filled];");
		}
	}

	private void printEdgesInternalOverriden(PrintStream out, JBddNode node,
			Set<JBddNode> visited) {
		if (visited.contains(node))
			return;
		visited.add(node);

		if (!node.isConst()) {
			for (int i = 0; i < node.getLevel(); i++)
				out.print("\t");
			out.print(node.getUniqueId() + "[" + node.getLevel() + "];");
		} else {
			out.print(node.getUniqueId() + "[" + node + "]");
		}

		if (!node.isConst()) {
			out.print(" -> [low]" + node.low.getUniqueId());
			out.println(" -> [high] " + node.high.getUniqueId());
			printEdgesInternalOverriden(out, node.high, visited);
			printEdgesInternalOverriden(out, node.low, visited);
		} else {
			out.println(node.getUniqueId() + "[box]");
		}
	}

	private void printBreadthFirstTraversal(PrintWriter out, JBddNode root,
			Set<JBddNode> visited) {
		int depth, prevIndex = -1;
		depth = getBDDDepth(root, 0);
		LinkedList<JBddNode> queue = new LinkedList<JBddNode>();
		queue.addLast(root);

		while (!queue.isEmpty()) {
			JBddNode current = queue.removeFirst();
			if (!current.isConst()) {

				queue.addLast(current.low);
				queue.addLast(current.high);
				if (!visited.contains(current)) {
					if (prevIndex != current.getLevel()) {
						out.println();
						for (int i = 0; i < depth - current.getLevel(); i++) {
							out.print("\t");
						}
						out.print(current.toString() + ","
								+ current.low.toString() + ","
								+ current.high.toString());
					} else {
						out.print("\t\t" + current.toString() + ","
								+ current.low.toString() + ","
								+ current.high.toString());
					}
					visited.add(current);
					prevIndex = current.getLevel();
				}
			}
		}
	}

	private int getBDDDepth(JBddNode node, int depth) {
		if (!node.isConst()) {
			return Math.max(getBDDDepth(node.low, depth + 1), getBDDDepth(
					node.high, depth + 1));
		}
		return depth;
	}

	// /////////////////////////////////////////
	// overrides methods from java.lang.Object
	// /////////////////////////////////////////
	public int hashCode() {
		return this.root.hashCode();
	}

	public boolean equals(Object other) {
		if (other instanceof JBDD) {
			JBDD otherBdd = (JBDD) other;
			return this.bddm == otherBdd.bddm && this.root == otherBdd.root;
		}
		return false;
	}

	public String toString() {
		return this.root.toString();
	}

	private JBddManager bddm; // its manager
	private JBddNode root; // the root node
}
